X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=5d1ea50962f211c333732ebc1fafb1622194b640;hb=0e4dbb2c911e538fcb8c8260c7d3e2be1bcc5b1e;hp=5f64b1b0a91384c9fb77b7e34f1db2ccf30357c5;hpb=779859f7a9e317e378d258897c289f447adea7ad;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 5f64b1b0a..5d1ea5096 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -475,7 +475,10 @@ let basic_eval_unification_hint (t,n) status =
 ;;
 
 let inject_unification_hint =
- let basic_eval_unification_hint (t,n) ~refresh_uri_in_term =
+ let basic_eval_unification_hint (t,n) 
+   ~refresh_uri_in_universe 
+   ~refresh_uri_in_term
+ =
   let t = refresh_uri_in_term t in basic_eval_unification_hint (t,n)
  in
   NRstatus.Serializer.register "unification_hints" basic_eval_unification_hint
@@ -488,6 +491,29 @@ let eval_unification_hint status t n =
  let t = NCicUntrusted.apply_subst subst [] t in
  let status = basic_eval_unification_hint (t,n) status in
  let dump = inject_unification_hint (t,n)::status#dump in
+ let status = status#set_dump dump in
+  status,`New []
+;;
+
+let basic_eval_add_constraint (s,u1,u2) status =
+ NCicLibrary.add_constraint status s u1 u2
+;;
+
+let inject_constraint =
+ let basic_eval_add_constraint (s,u1,u2) 
+       ~refresh_uri_in_universe 
+       ~refresh_uri_in_term
+ =
+  let u1 = refresh_uri_in_universe u1 in 
+  let u2 = refresh_uri_in_universe u2 in 
+  basic_eval_add_constraint (s,u1,u2)
+ in
+  NRstatus.Serializer.register "constraints" basic_eval_add_constraint
+;;
+
+let eval_add_constraint status s u1 u2 = 
+ let status = basic_eval_add_constraint (s,u1,u2) status in
+ let dump = inject_constraint (s,u1,u2)::status#dump in
  let status = status#set_dump dump in
   status,`Old []
 ;;
@@ -699,14 +725,12 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
           | _ -> obj_kind
         in
         let obj = uri,height,[],[],obj_kind in
-         NCicTypeChecker.typecheck_obj obj;
-         let status = NCicLibrary.add_obj status uri obj in
+         let status = NCicLibrary.add_obj status obj in
          let objs = NCicElim.mk_elims obj in
          let timestamp,uris_rev =
            List.fold_left
             (fun (status,uris_rev) (uri,_,_,_,_) as obj ->
-              NCicTypeChecker.typecheck_obj obj;
-              let status = NCicLibrary.add_obj status uri obj in
+              let status = NCicLibrary.add_obj status obj in
                status,uri::uris_rev
             ) (status,[]) objs in
          let uris = uri::List.rev uris_rev in
@@ -729,8 +753,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
            eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
         | _ -> status,`New [])
   | GrafiteAst.NUnivConstraint (loc,strict,u1,u2) ->
-      NCicEnvironment.add_constraint strict [false,u1] [false,u2];
-      status, `New [u1;u2]
+      eval_add_constraint status strict [false,u1] [false,u2]
 ;;
 
 let rec eval_command = {ec_go = fun ~disambiguate_command opts status