improved check in delift for flexible lc entries.

[helm.git] / helm / software / components / grafite_engine / grafiteEngine.ml

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index f7df56315e235a5e42d179579e546c824f7020ce..ec9f3866fdab4bbffab2ce894ab17e937b809cef 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -41,6 +41,11 @@ type options = {
   do_heavy_checks: bool ; 
 }
 
+let concat_nuris uris nuris =
+   match uris,nuris with
+   | `New uris, `New nuris -> `New (nuris@uris)
+   | _ -> assert false
+;;
 (** create a ProofEngineTypes.mk_fresh_name_type function which uses given
   * names as long as they are available, then it fallbacks to name generation
   * using FreshNamesGenerator module *)
@@ -767,9 +772,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
                  eval_ncommand opts status
                   ("",0,GrafiteAst.NObj (HExtlib.dummy_floc,boxml))
                 in
-                 match uris,nuris with
-                    `New uris, `New nuris -> status,`New (nuris@uris)
-                  | _ -> assert false
+                status, concat_nuris uris nuris
                with
                 NCicTypeChecker.TypeCheckerFailure msg
                  when Lazy.force msg =
@@ -785,16 +788,21 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
                  (fun (name,is_coercion,arity) ->
                    if is_coercion then Some(name,leftno,arity) else None) fields
             | _ -> [] in
-           let status =
+           let status,uris =
             List.fold_left
-             (fun status (name,cpos,arity) ->
+             (fun (status,uris) (name,cpos,arity) ->
                let metasenv,subst,status,t =
                 GrafiteDisambiguate.disambiguate_nterm None status [] [] []
                  ("",0,CicNotationPt.Ident (name,None)) in
                assert (metasenv = [] && subst = []);
-               NCicCoercDeclaration.basic_eval_and_inject_ncoercion_from_t_cpos_arity 
-                 status (name,t,cpos,arity)
-             ) status coercions
+               let status, nuris = 
+                 NCicCoercDeclaration.
+                   basic_eval_and_record_ncoercion_from_t_cpos_arity 
+                    status (name,t,cpos,arity)
+               in
+               let uris = concat_nuris nuris uris in
+               status, uris) 
+             (status,uris) coercions
            in
             status,uris
           with