From 2596b5aa335f8763ecd0f9263df7d538f0958e59 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 2 Dec 2010 16:16:49 +0000 Subject: [PATCH] Bad default for ?dorefine for instantiate --- helm/software/components/ng_tactics/nTacStatus.ml | 2 +- helm/software/components/ng_tactics/nTacStatus.mli | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml index 4a7f98196..e7d5bb3b5 100644 --- 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 edaf40b6c..416306c02 100644 --- 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 -- 2.39.2