an option to retain old prop typing; fix a regression test that insta…

…ntiates existential quanitifers "magically"

src/smtencoding/FStar.SMTEncoding.Encode.fst

@@ -821,7 +821,7 @@ let encode_top_level_let :
                     let app_is_prop = Term.mk_subtype_of_unit app in
                     if should_encode_logical
                     then (
-                      if is_sub_singleton
+                      if is_sub_singleton && Options.Ext.get "retain_old_prop_typing" = ""
                       then (
                         Util.mkAssume(mkForall (S.range_of_lbname lbn)
                                             ([[app_is_prop]], vars, mk_Valid <| app_is_prop),

src/smtencoding/FStar.SMTEncoding.Pruning.fst

@@ -461,4 +461,8 @@ let prune (p:pruning_state) (roots:list decl)
         | Some a -> [a]) 
       (reached_names@p.ambients)
   in
+  // if Options.Ext.get "debug_context_pruning" <> ""
+  // then (
+  //   BU.print1 "Retained %s assumptions\n" (show (List.length reached_assumptions))
+  // );
   reached_assumptions

tests/bug-reports/Bug2172.fst

@@ -1,14 +1,11 @@
 module Bug2172
 #push-options "--ext context_pruning"
 // one existential quantification over two variables (`p2` below) is
-// different from two extistential quantifications over one variable
+// different from two existential quantifications over one variable
 // each (`p1` below)
 let p1 = exists (x: int). exists (y: int). 0 == x + y
 let p2 = exists (x: int)         (y: int). 0 == x + y
 
 let test0 (witness:nat) = assert p1
-#pop-options
-#push-options "--ext 'context_pruning='"
-let test1 = assert p2
-#pop-options
+let test1 (x:int) = assert (0 == x + (-x)); assert p2
 let _ = assert (p1 <==> p2)