The Aux argument of conclude is now of type string (used to be int).

[helm.git] / helm / ocaml / cic_omdoc / cic2content.ml

diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml
index 2749708d2018ec609e8132f689d02f40ad9e781a..149fd90ec4389dfb47015cbb16dc2803e976fcf3 100644 (file)
--- a/helm/ocaml/cic_omdoc/cic2content.ml
+++ b/helm/ocaml/cic_omdoc/cic2content.ml
@@ -465,46 +465,50 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
           generate_exact seed t id name ~ids_to_inner_types
         else raise Not_a_proof
     | C.AMutCase (id,uri,typeno,ty,te,patterns) ->
+        let inductive_types =
+           (match CicEnvironment.get_obj uri with
+               Cic.Constant _ -> assert false
+             | Cic.Variable _ -> assert false
+             | Cic.CurrentProof _ -> assert false
+             | Cic.InductiveDefinition (l,_,_) -> l 
+           ) in
+        let (_,_,_,constructors) = List.nth inductive_types typeno in 
         let teid = get_id te in
-        let pp = List.map (function p -> (K.ArgProof (aux p))) patterns in
-        (match 
-          (try Some (Hashtbl.find ids_to_inner_types teid).C2A.annsynthesized
-           with Not_found -> None)
-         with
-             Some tety -> (* we must lift up the argument *)
+        let pp = List.map2 
+          (fun p (name,_) -> (K.ArgProof (aux ~name p))) 
+           patterns constructors in
+        let apply_context,term =
+          (match 
+            (try Some (Hashtbl.find ids_to_inner_types teid).C2A.annsynthesized
+             with Not_found -> None)
+           with
+             Some tety -> 
                let p = (aux te) in
-               { K.proof_name = Some "name";
-                 K.proof_id   = gen_id seed;
-                 K.proof_context = []; 
-                 K.proof_apply_context = flat seed p;
-                 K.proof_conclude = 
-                   { K.conclude_id = gen_id seed; 
-                     K.conclude_aref = id;
-                     K.conclude_method = "Case";
-                     K.conclude_args = (K.Term ty)::(K.Term te)::pp;
-                     K.conclude_conclusion = 
-                       try Some 
-                        (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
-                       with Not_found -> None  
-                   }
-               }
-           | None ->
-               { K.proof_name = name;
-                 K.proof_id   = gen_id seed;
-                 K.proof_context = []; 
-                 K.proof_apply_context = [];
-                 K.proof_conclude = 
-                   { K.conclude_id = gen_id seed; 
-                     K.conclude_aref = id;
-                     K.conclude_method = "Case";
-                     K.conclude_args = (K.Term ty)::(K.Term te)::pp;
-                     K.conclude_conclusion = 
-                       try Some 
-                        (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
-                       with Not_found -> None 
-                   }
-               }
-         )  
+               (flat seed p, 
+                K.Premise
+                { K.premise_id = gen_id seed; 
+                   K.premise_xref = p.K.proof_id;
+                   K.premise_binder = p.K.proof_name;
+                   K.premise_n = None
+                 })
+           | None -> [],K.Term te) in
+        { K.proof_name = name;
+          K.proof_id   = gen_id seed;
+          K.proof_context = []; 
+          K.proof_apply_context = apply_context;
+          K.proof_conclude = 
+            { K.conclude_id = gen_id seed; 
+              K.conclude_aref = id;
+              K.conclude_method = "Case";
+              K.conclude_args = 
+                (K.Aux (UriManager.string_of_uri uri))::
+                (K.Aux (string_of_int typeno))::(K.Term ty)::term::pp;
+              K.conclude_conclusion = 
+                try Some 
+                  (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
+                with Not_found -> None  
+             }
+        }
     | C.AFix (id, no, funs) -> 
         let proofs = 
           List.map 
@@ -696,7 +700,7 @@ and inductive seed name id li ids_to_inner_types ids_to_inner_sorts =
                 K.conclude_aref = id;
                 K.conclude_method = "ByInduction";
                 K.conclude_args =
-                  K.Aux no_constructors 
+                  K.Aux (string_of_int no_constructors) 
                   ::K.Term (C.AAppl id ((C.AConst(idc,uri,exp_named_subst))::params_and_IP))
                   ::method_args@other_method_args;
                 K.conclude_conclusion =