X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=7cf3897faf2ffe697a7e2df1c03228e57de783bc;hb=d175eb77ca53f7f11377fada4b964ef6c4d0a592;hp=d9c4608492dc9e02e6d664265ec2bfbfb9628d79;hpb=154cbc049da8d8c3dd090a919a40c90eb23cc24e;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index d9c460849..7cf3897fa 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -427,6 +427,16 @@ type 'a eval_command =
    GrafiteTypes.status * UriManager.uri list
  }
 
+type 'a eval_comment =
+ {ecm_go: 'term 'lazy_term 'reduction_kind 'obj 'ident.
+  disambiguate_command:
+   (GrafiteTypes.status -> (('term,'obj) GrafiteAst.command) disambiguator_input ->
+    GrafiteTypes.status * (Cic.term,Cic.obj) GrafiteAst.command) -> 
+  options -> GrafiteTypes.status -> 
+    (('term,'lazy_term,'reduction_kind,'obj,'ident) GrafiteAst.comment) disambiguator_input ->
+   GrafiteTypes.status * UriManager.uri list
+ }
+
 type 'a eval_executable =
  {ee_go: 'term 'lazy_term 'reduction 'obj 'ident.
   disambiguate_tactic:
@@ -482,7 +492,13 @@ let refinement_toolkit = {
   RefinementTool.ppmetasenv = CicMetaSubst.ppmetasenv; 
   RefinementTool.pack_coercion_obj = CicRefine.pack_coercion_obj;
  }
-  
+ 
+let eval_unification_hint status t = 
+  (* XXX no undo *)        
+  NCicUnifHint.add_user_provided_hint t;
+  status,[]
+;;
+
 let eval_coercion status ~add_composites uri arity saturations =
  let uri = 
    try CicUtil.uri_of_term uri 
@@ -554,13 +570,11 @@ let eval_tactical status tac =
   in
   status
 
-let eval_comment status c = status
-
 (* since the record syntax allows to declare coercions, we have to put this
  * information inside the moo *)
 let add_coercions_of_record_to_moo obj lemmas status =
   let attributes = CicUtil.attributes_of_obj obj in
-  let is_record = function `Class (`Record att) -> Some att | _-> None in
+  let is_record x _ = match x with `Class (`Record att) -> Some att | _-> None in
   match HExtlib.list_findopt is_record attributes with
   | None -> status,[]
   | Some fields -> 
@@ -656,6 +670,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
       status,[] 
   | GrafiteAst.Coercion (loc, uri, add_composites, arity, saturations) ->
      eval_coercion status ~add_composites uri arity saturations 
+  | GrafiteAst.UnificationHint (loc, t) ->
+     eval_unification_hint status t
   | GrafiteAst.Default (loc, what, uris) as cmd ->
      LibraryObjects.set_default what uris;
      GrafiteTypes.add_moo_content [cmd] status,[]
@@ -853,7 +869,12 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
   | GrafiteAst.Executable (_,ex) ->
      eval_executable.ee_go ~disambiguate_tactic ~disambiguate_command
       ~disambiguate_macro opts status (text,prefix_len,ex)
-  | GrafiteAst.Comment (_,c) -> eval_comment status (text,prefix_len,c),[]
+  | GrafiteAst.Comment (_,c) -> 
+      eval_comment.ecm_go ~disambiguate_command opts status (text,prefix_len,c) 
+} and eval_comment = { ecm_go = fun ~disambiguate_command opts status (text,prefix_len,c) -> 
+    status, []
 }
+;;
+
 
 let eval_ast = eval_ast.ea_go