Bad default for ?dorefine for instantiate

diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml
index 4a7f9819650b0efa11954f27017129a1b43aefa5..e7d5bb3b532ee1eac2b6fdcee560ad8b58cb61c2 100644 (file)
--- a/helm/software/components/ng_tactics/nTacStatus.ml
+++ b/helm/software/components/ng_tactics/nTacStatus.ml
@@ -249,7 +249,7 @@ let to_subst status i entry =
   status#set_obj (name,height,metasenv,subst,obj)
 ;;
 
-let instantiate status ?refine:(dorefine=false) i t =
+let instantiate status ?refine:(dorefine=true) i t =
  let _,_,metasenv,_,_ = status#obj in
  let gname, context, gty = List.assoc i metasenv in
   if dorefine then

diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli
index edaf40b6cf2578697ad3534a2a797934c22bb8cf..416306c021f3021638d437361ddb4c81db1fd19b 100644 (file)
--- a/helm/software/components/ng_tactics/nTacStatus.mli
+++ b/helm/software/components/ng_tactics/nTacStatus.mli
@@ -77,7 +77,7 @@ val mk_meta:
    [ `Decl of cic_term | `Def of cic_term ] -> NCicUntrusted.meta_kind ->
      'status * cic_term
 
-(* default value for refine: false; you can use true if the term has already been refined with
+(* default value for refine: true; you can use false if the term has already been refined with
    the expected type for the meta (e.g. after a reduction tactic) *)
 val instantiate: #pstatus as 'status -> ?refine:bool -> int -> cic_term -> 'status
 val instantiate_with_ast: #pstatus as 'status -> int -> tactic_term -> 'status