Program: cleanup in cases, add options

Unset Program Generalized Coercion to avoid coercion of general
applications.
Unset Program Cases to deactivate generation equalities and
disequalities of cases.

5 files changed, 38 insertions, 25 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 205a199f7..78c218a50 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1801,14 +1801,10 @@ let build_inversion_problem loc env sigma tms t =
 	          it = None } } ] in
   (* [pb] is the auxiliary pattern-matching serving as skeleton for the
       return type of the original problem Xi *)
-  (* let sigma, s = Evd.new_sort_variable sigma in *)
-(*FIXME TRY *)
-  (* let sigma, s = Evd.new_sort_variable univ_flexible sigma in *)
   let s' = Retyping.get_sort_of env sigma t in
   let sigma, s = Evd.new_sort_variable univ_flexible_alg sigma in
   let sigma = Evd.set_leq_sort env sigma s' s in
   let evdref = ref sigma in
-  (* let ty = evd_comb1 (refresh_universes false) evdref ty in *)
   let pb =
     { env       = pb_env;
       evdref    = evdref;
@@ -1944,7 +1940,7 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
 let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
   let preds =
     match pred, tycon with
-    (* No type annotation *)
+    (* No return clause *)
     | None, Some t when not (noccur_with_meta 0 max_int t) ->
 	(* If the tycon is not closed w.r.t real variables, we try *)
         (* two different strategies *)
@@ -1981,12 +1977,6 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
       let evdref = ref sigma in
       let predcclj = typing_fun (mk_tycon (mkSort newt)) envar evdref rtntyp in
       let sigma = !evdref in
-      (* let sigma = Option.cata (fun tycon -> *)
-      (*     let na = Name (Id.of_string "x") in *)
-      (*     let tms = List.map (fun tm -> Pushed(tm,[],na)) tomatchs in *)
-      (*     let predinst = extract_predicate predcclj.uj_val tms in *)
-      (*     Coercion.inh_conv_coerce_to loc env !evdref predinst tycon) *)
-      (*   !evdref tycon in *)
       let predccl = (j_nf_evar sigma predcclj).uj_val in
       [sigma, predccl]
   in
@@ -2436,7 +2426,7 @@ let compile_program_cases loc style (typing_function, evdref) tycon env
     match tycon' with
     | None -> let ev = mkExistential env evdref in ev, ev
     | Some t ->
-	let pred = 
+	let pred =
 	  match prepare_predicate_from_arsign_tycon env !evdref loc tomatchs sign t with
 	  | Some (evd, pred) -> evdref := evd; pred
 	  | None ->
@@ -2515,11 +2505,11 @@ let compile_program_cases loc style (typing_function, evdref) tycon env
 (* Main entry of the matching compilation                                 *)
 
 let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, eqns) =
-  if predopt == None && Flags.is_program_mode () then
-    compile_program_cases loc style (typing_fun, evdref) 
+  if predopt == None && Flags.is_program_mode () && Program.is_program_cases () then
+    compile_program_cases loc style (typing_fun, evdref)
       tycon env (predopt, tomatchl, eqns)
   else
-      
+
   (* We build the matrix of patterns and right-hand side *)
   let matx = matx_of_eqns env eqns in
 
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index d7fff8af4..ba566f374 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -121,4 +121,3 @@ val prepare_predicate :            Loc.t ->
            Context.Rel.t list ->
            Constr.constr option ->
            'a option -> (Evd.evar_map * Names.name list * Term.constr) list
-
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index cba28f817..65d79bcc8 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -192,7 +192,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
 	  let term = co x in
 	    Typing.e_solve_evars env evdref term)
       in
-	if isEvar c || isEvar c' then
+	if isEvar c || isEvar c' || not (Program.is_program_generalized_coercion ()) then
 	  (* Second-order unification needed. *)
 	  raise NoSubtacCoercion;
 	aux [] typ typ' 0 (fun x -> x)
@@ -280,7 +280,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
 		     let c1 = coerce_unify env a a' in
 		     let c2 = coerce_unify env b b' in
 		       match c1, c2 with
-		       None, None -> None
+		       | None, None -> None
 		       | _, _ ->
 			   Some
 			     (fun x ->
diff --git a/pretyping/program.ml b/pretyping/program.ml
index 133f83090..253d85742 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -70,18 +70,40 @@ let mk_coq_and l =
 
 (* true = transparent by default, false = opaque if possible *)
 let proofs_transparency = ref true
+let program_cases = ref true
+let program_generalized_coercion = ref true
 
 let set_proofs_transparency = (:=) proofs_transparency
 let get_proofs_transparency () = !proofs_transparency
 
+let is_program_generalized_coercion () = !program_generalized_coercion
+let is_program_cases () = !program_cases
+
 open Goptions
 
 let _ =
   declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
-      optname  = "preferred transparency of Program obligations";
-      optkey   = ["Transparent";"Obligations"];
-      optread  = get_proofs_transparency;
-      optwrite = set_proofs_transparency; }
-      
+  { optsync  = true;
+    optdepr  = false;
+    optname  = "preferred transparency of Program obligations";
+    optkey   = ["Transparent";"Obligations"];
+    optread  = get_proofs_transparency;
+    optwrite = set_proofs_transparency; }
+
+let _ =
+  declare_bool_option
+  { optsync  = true;
+    optdepr  = false;
+    optname  = "program cases";
+    optkey   = ["Program";"Cases"];
+    optread  = (fun () -> !program_cases);
+    optwrite = (:=) program_cases }
+
+let _ =
+  declare_bool_option
+  { optsync  = true;
+    optdepr  = false;
+    optname  = "program generalized coercion";
+    optkey   = ["Program";"Generalized";"Coercion"];
+    optread  = (fun () -> !program_generalized_coercion);
+    optwrite = (:=) program_generalized_coercion }
diff --git a/pretyping/program.mli b/pretyping/program.mli
index 765f35580..023ff8ca5 100644
--- a/pretyping/program.mli
+++ b/pretyping/program.mli
@@ -39,3 +39,5 @@ val mk_coq_not : constr -> constr
 val papp : Evd.evar_map ref -> (unit -> global_reference) -> constr array -> constr
 
 val get_proofs_transparency : unit -> bool
+val is_program_cases : unit -> bool
+val is_program_generalized_coercion : unit -> bool